Publications of Jean-Paul BODEVEIX
Zhibin Yang, Zhikai Qiu, Yong Zhou, Zhiqiu Huang, Jean-Paul Bodeveix, M Filali
C2AADL_Reverse: A model-driven reverse engineering approach to development and verification of safety-critical software
Journal of Systems Architecture, 2021, 118, pp.102202. ⟨10.1016/j.sysarc.2021.102202⟩
Zhibin Yang, Shenghao Yuan, Jean-Paul Bodeveix, M Filali, Tiexin Wang, Yong Zhou
Multi-task Ada code generation from synchronous dataflow programs on multi-core: Approach and industrial study
Science of Computer Programming, 2021, Special issue:SI: Formal Techniques for Safety-Critical Systems 2019, 207, pp.102644. ⟨10.1016/j.scico.2021.102644⟩
Zhibin Yang, Yang Bao, Yongqiang Yang, Zhiqiu Huang, Jean-Paul Bodeveix, M Filali, Zonghua Gu
Exploiting augmented intelligence in the modeling of safety-critical autonomous systems
Formal Aspects of Computing, 2021, 33 (3), pp.343-384. ⟨10.1007/s00165-021-00543-6⟩
Jean-Paul Bodeveix, Arnaud Dieumegard, M Filali
Event-B formalization of a variability-aware component model patterns framework
Science of Computer Programming, 2020, 199, ⟨10.1016/j.scico.2020.102511⟩
Fei Wang, Zhibin Yang, Zhi-Qiu Huang, Cheng-Wei Liu, Yong Zhou, Jean-Paul Bodeveix, M Filali
An Approach to Generate the Traceability Between Restricted Natural Language Requirements and AADL Models
IEEE Transactions on Reliability, 2019, 1 (1), pp.1-20. ⟨10.1109/TR.2019.2936072⟩
Zhibin Yang, Jean-Paul Bodeveix, M Filali
Towards a simple and safe Objective Caml compiling framework for the synchronous language SIGNAL
Frontiers of Computer Science, 2019, 13 (4), pp.715-734. ⟨10.1007/s11704-017-6485-y⟩
Elie Fares, Jean-Paul Bodeveix, M Filali
Event algebra for transition systems composition Application to timed automata
Acta Informatica, 2018, 55, pp.363-400. ⟨10.1007/s00236-017-0302-9⟩
Zhibin Yang, Jean-Paul Bodeveix, M Filali, Kai Hu, Yongwang Zhao, Dianfu Ma
Towards a verified compiler prototype for the synchronous language SIGNAL
Frontiers of Computer Science, 2016, 10 (1), pp.37-53. ⟨10.1007/s11704-015-4364-y⟩
Jean-Paul Bodeveix, M Filali, Manuel Garnacho, Régis Spadotti, Zhibin Yang
Towards a verified transformation from AADL to the formal component-based language FIACRE
Science of Computer Programming, 2015, vol. 106, pp. 30-53. ⟨10.1016/j.scico.2015.03.003⟩
Zhibin Yang, Kai Hu, Yong-Wang Zhao, Dian-Fu Ma, Jean-Paul Bodeveix
Verification of AADL Models with Timed Abstract State Machines
Journal of Software, 2015, vol. 26 (n° 2), pp. 202-222
Zhibin Yang, Kai Hu, Dianfu Ma, Jean-Paul Bodeveix, Lei Pi, Jean-Pierre Talpin
From AADL to Timed Abstract State Machines: A Verified Model Transformation
Journal of Systems and Software, 2014, vol. 93, pp. 42-68. ⟨10.1016/j.jss.2014.02.058⟩
Zhibin Yang, Kai Hu, Dianfu Ma, Jean-Paul Bodeveix, Lei Pi, Jean-Pierre Talpin
From AADL to timed abstract state machine: a certified model transformation
Journal of Systems and Software, 2014, Journal of Systems and Software, pp.20
Zhibin Yang, Jean-Paul Bodeveix, Mamoun Filali
A comparative study of two formal semantics of the SIGNAL language
In : Frontiers of Computer Science, Springer, Vol. 7 N. 5, pp. 673-693, October 2013.
Jean-Paul Bodeveix, Mamoun Filali
Event B Development of a Synchronous AADL Scheduler
In : Electronic Notes in Theoretical Computer Science (ENTCS), Elsevier, Special issue Proceedings of the B 2011 Workshop, a satellite event of the 17th International Symposium on Formal Methods (FM 2011), Vol. 280, pp. 23-33, December 2011.
URL : http://www.sciencedirect.com/science/article/pii/S1571066111001642
BibTeXOdile Nasr, Miloud Rached, Jean-Paul Bodeveix, Mamoun Filali
Spécification et vérification d’un ordonnanceur en B via les automates temporisés
In : L’Objet, Hermès Science, Special issue Composants, services et aspects techniques et outils pour la vérification, Vol. 14, N. 4, pp. 43-72, December 2008.
Miloud Rached, Odile Nasr, Jean-Paul Bodeveix, Mamoun Filali
Une Extension Temporisée de la Méthode B pour la Spécification et la Vérification des Systèmes Temps-Réel
In : Journal Européen des Systèmes Automatisés (JESA), Hermès Science, Special issue Approches formelles pour la spécification et la verification des systèmes embarqués temps-réel, Vol. 42 N. 9, pp. 1061-1084, December 2008.
Jean-Paul Bodeveix, Mamoun Filali, Julia Lawall, Gilles Muller
Automatic Verification of Bossa Scheduler Properties
In : Electronic Notes in Theoretical Computer Science (ENTCS), Elsevier, Vol. 185, pp. 17-32, July 2007.
Jean-Paul Bodeveix, David Chemouil, Mamoun Filali, Martin Strecker
Towards formalising AADL in Proof Assistants
In : Electronic Notes in Theoretical Computer Science (ENTCS), Elsevier, Vol. 141, pp. 153-169, August 2005.
Richard Banach, Jean-Paul Bodeveix, Mamoun Filali, Michael Poppleton
Dynamic aspects of retrenchments through temporal logic
In : Annals of Mathematics, Computing and Teleinformatics (AMCT), Technological Education Institute of Larissa, Grèce, Vol. 1 N. 3, pp. 18-26, 2005.
Jean-Paul Bodeveix, Mamoun Filali
Reduction and quantifier elimination techniques for program validation
In : Formal Methods in System Design, Vol. 20 N. 1, pp. 69-89, 2002.
Jean-Paul Bodeveix, Mamoun Filali, Cesar Munoz
Formalisation de la méthode B en Coq et PVS
In : Technique et Science Informatiques, HERMES, PARIS, Vol. 20, N. 7, pp. 901-926, July 2001.
Didier Plaindoux, Jean-Paul Bodeveix, Christian Percebois
Types versus Classes
In : L’Objet, Hermes, Vol. 4, N. 1, pp. 3-25, 1998.
Jean-Paul Bodeveix, Mamoun Filali
Techniques de preuve automatique pour la validation de programmes
In : Technique et science informatiques, hermes, Paris, Vol. 17, N. 9, pp. 1129-1155, November 1998.
Jean-Paul Bodeveix, Mamoun Filali
Towards the automatic verification of atomic memory protocols
In : Parallel Processing Letter, M. Cosnard, Vol. 7 N. 1, pp. 101-112, 1997.
Quentin Peyras, Jean-Paul Bodeveix, Julien Brunel, David Chemouil
Sound Verification Procedures for Temporal Properties of Infinite-State Systems
33rd International Conference on Computer-Aided Verification (CAV 2021), Jul 2021, Los Angeles (Online), United States
Jian Zhu, Kai Hu, Jean-Paul Bodeveix, M Filali, Jean-Pierre Talpin, Haitao Cao
Formal Simulation and Verification of Solidity contracts in Event-B
45th IEEE Annual Computers, Software, and Applications Conference (COMPSAC 2021), IEEE, Jul 2021, Madrid, Spain. pp.1309-1314, ⟨10.1109/COMPSAC51774.2021.00183⟩
Event-B Formalization of Event-B Contexts
8th International Conference on Rigorous State-Based Methods (ABZ 2021), Jun 2021, Ulm, Germany. pp.66-80, ⟨10.1007/978-3-030-77543-8_5⟩
Jean-Paul Bodeveix, Julien Brunel, David Chemouil, M Filali
Mechanically Verifying the Fundamental Liveness Property of the Chord Protocol
23rd International Symposium on Formal Methods (FM 2019), FME: Formal Methods Europe, Oct 2019, Porto, Portugal. pp.45-63, ⟨10.1007/978-3-030-30942-8_5⟩
Jean-Paul Bodeveix, Arnaud Dieumegard, M Filali
Event-B Formalization of a Variability-Aware Component Model Patterns Framework
15th International Conference on Formal Aspects of Component Software (FACS 2018), Oct 2018, Pohang, South Korea. pp.54-74, ⟨10.1007/978-3-030-02146-7_3⟩
Jean-Paul Bodeveix, Arnaud Dieumegard, M Filali
Pattern-based requirements development
9th European Congress on Embedded Real Time Software and Systems (ERTS 2018), Jan 2018, Toulouse, France
Jean-Paul Bodeveix, M Filali, Shuanglong Kan
A Refinement-based compiler development for synchronous languages
15th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE 2017), Sep 2017, Vienna, Austria. pp.165-174, ⟨10.1145/3127041.3127056⟩
Jean-Paul Bodeveix, M Filali, Shuanglong Kan
A refinement-based compiler development for synchronous languages
15th International Conference on Formal Methods and Models for System Design (MEMOCODE 2017), ACM; SIGBED; SIGDA; IEEE CEDA; IEEE CAS, Sep 2017, Vienne, Austria. pp.165-174, ⟨10.1145/3127041.3127056⟩
Badr Siala, Jean-Paul Bodeveix, M Filali, Tahar Bhiri
Automatic Refinement for Event-B through Annotated Patterns
25th Euromicro International Conference on Parallel, Distributed and network-based Processing (PDP 2017), Mar 2017, Saint Petersburg, Russia. pp.287-290, ⟨10.1109/PDP.2017.72⟩
Badr Siala, Tahar Bhiri, Jean-Paul Bodeveix, M Filali
An Event-B Development Process for the Distributed BIP Framework
18th International Conference on Formal Engineering Methods (ICFEM 2016), Nov 2016, Tokyo, Japan. pp. 313-328
Badr Siala, Mohamed Tahar Bhiri, Jean-Paul Bodeveix, M Filali
Un processus de développement Event-B pour des applications distribuées
15emes Journéees Approches Formelles dans l’Assistance au Développement de Logiciels (AFADL 2016), en collaboration avec les journées du GDR GPL, Jun 2016, Besançon, France. pp.94-100
Badr Siala, Tahar Bhiri, Jean-Paul Bodeveix, M Filali
An Event-B development process for the distributed BIP framework (Journées FAC Toulouse 2016)
Journées Formalisation des Activités Concurrentes (FAC 2016), Groupe IFSE du RTRA STAE (Réseau Thématique de Recherche Avancée « Sciences et Technologies pour l’Aéronautique et l’Espace » de Toulouse), Mar 2016, Toulouse, France
Zhibin Yang, Jean-Paul Bodeveix, M Filali
Multi-core Code Generation from Polychronous Programs with Time-Predictable Properties (ACVI 2014)
1st International Workshop on Architecture Centric Virtual Integration (ACVI 2014), Sep 2014, Valencia, Spain. pp.1-10
Zhibin Yang, Jean-Paul Bodeveix, M Filali, Kai Hu, Dianfu Ma
A Verified Transformation: From Polychronous Programs to a Variant of Clocked Guarded Actions
17th International Workshop on Software and Compilers for Embedded Systems (SCOPES 2014), SIGBED: Special Interest Group on Embedded Systems, Jun 2014, Sankt Goar, Germany. pp.128-137, ⟨10.1145/2609248.2609259⟩
Elie Fares, Jean-Paul Bodeveix, Mamoun Filali
Event Algebra for Transition Systems Composition – Application to Timed Automata (regular paper)
In : International Symposium on Temporal Representation and Reasoning (TIME 2013), Penscacolq, FL, USA, 26/09/13-28/09/13, IEEE Computer Society – Conference Publishing Services, pp. 125-132, 2013.
Elie Fares, Jean-Paul Bodeveix, Mamoun Filali, Manuel Garnacho
An Automatic Technique for Checking the Simulation of Timed Systems (regular paper)
In : Automated Technology for Verification and Analysis, Hanoi, Vietnam, 15/10/13-18/10/13, Vol. 8172, Springer-Verlag, Lecture Notes in Computer Science, pp. 71-86, October 2013.
Abdeldjalil Boudjadar, Frits Vaandrager, Jean-Paul Bodeveix, Mamoun Filali
Extending UPPAAL for the Modeling and Verification of Dynamic Real-Time Systems (regular paper)
In : Fundamentals of Software Engineering (FSEN 2013), Tehran, Iran, 24/04/13-26/04/13, Vol. 8161, Springer, Lecture Notes in Computer Science, pp. 111-132, April 2013.
Manuel Garnacho, Jean-Paul Bodeveix, Mamoun Filali
A Mechanized Semantic Framework for Real-Time Systems (regular paper)
In : International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS 2013), Buenos Aires, Argentina, 29/08/13-31/08/13, Victor Braberman, Laurent Fribourg (Eds.), Springer, pp. 106-120, August 2013.
Abdeldjalil Boudjadar, Jean-Paul Bodeveix, Mamoun Filali
Compositional Refinement for Real-Time Systems with Priorities (regular paper)
In : International Symposium on Temporal Representation and Reasoning (TIME 2012), Leicester, United Kingdom, 12/09/12-14/09/12, IEEE Computer Society, pp. 57-64, September 2012.
Bernard Berthomieu, Jean-Paul Bodeveix, Silvano Dal Zilio, Patrick Farail, Mamoun Filali, Pierre Gaufillet, François Vernadat
La traduction AADL-FIACRE: l’expérience TOPCASED (regular paper)
In : Approches Formelles dans l’Assistance au Développement de Logiciels (AFADL 2012), Grenoble, 11/01/12-13/01/12 (invited speaker), LCIS/LIG Grenoble, pp. 8-8, January 2012.
Elie Fares, Jean-Paul Bodeveix, Mamoun Filali
Design of a BPEL verification tool (regular paper)
In : International Workshop on Web Services and Formal Methods, Clermont-Ferrand, 01/09/11-02/09/11, Springer, pp. 95-109, February 2012.
Jean-Paul Bodeveix, Mamoun Filali
Event B development of a synchronous AADL scheduler (regular paper)
In : Workshop B 2011, colocated with FM 2011, Limerick, Ireland, 21/06/11-21/06/11, University of Limerick, (electronic medium), June 2011.
Jean-Paul Bodeveix, Abdeldjalil Boudjadar, Mamoun Filali
An Alternative Definition for Timed Automata Composition (regular paper)
In : Automated Technology for Verification and Analysis, Taipei, Taiwan, 11/10/11-14/10/11, Vol. 6996, Springer-Verlag, Lecture Notes in Computer Science, pp. 105-119, October 2011.
Elie Fares, Jean-Paul Bodeveix, Mamoun Filali
A Transformation and Verification Framework for BPEL
In : Services et Langages et modèles à l’exécution, LILLE GDR GPL, 10/06/11-10/06/11.
Marie de Roquemaurel, Jean-Paul Bodeveix, Mamoun Filali
Réécriture de contraintes OCL (regular paper)
In : Journées sur l’Ingénierie Dirigée par les Modèles (IDM 2011), Lille, 07/06/11-10/06/11, CNRS – GDR GPL, pp. 127-133, 2011.
Marie de Roquemaurel, Thomas Polacsek, Jean-François Rolland, Jean-Paul Bodeveix, Mamoun Filali
Assistance à la conception de modèles à l’aide de contraintes (regular paper)
In : Journées nationales du Groupement De Recherche CNRS du Génie de la Programmation et du Logiciel (GDR-GPL), Groupe de travail MFDL, Lille, 07/06/11-10/06/11, CNRS – GDR GPL, pp. 121-136, June 2011.
Elie Fares, Jean-Paul Bodeveix, Mamoun Filali
Verification of Timed BPEL 2.0 Models (regular paper)
In : Business Process Modeling, Development and Support (BPMDS 2011), London, 20/06/11-21/06/11, Terry Halpin, Selmin Nurcan, John Krogstie, Pnina Soffer, Erik Proper (Eds.), Springer, LNBIP 81, pp. 261-275, June 2011.
Zhibin Yang, Hu Kai, Jean-Paul Bodeveix, Lei Pi, Dianfu Ma, Jean-Pierre Talpin
Two formal semantics of a subset of AADL (regular paper)
In : UML&AADL, Las Vegas, 27/04/11-27/04/11, IEEE Computer Society, ICECCS ’11, pp. 344-349, April 2011.
Marie de Roquemaurel, Jean-Paul Bodeveix, Mamoun Filali, Frédéric Minot
Model design through constraint solving
In : TOPCASED DAYS, Toulouse, 02/02/11-04/02/11.
Tiago Correa, Leandro Becker, Jean-Paul Bodeveix, J.-M. Farines, Mamoun Filali, François Vernadat
Supporting the Design of Safety Critical Systems Using AADL (regular paper)
In : , Oxford, 22/03/10-26/03/10, IEEE Computer Society, pp. 331-336, March 2010.
Zhibin Yang, Kai Hu, Lei Pi, Jean-Paul Bodeveix, Dianfu Ma
Formal Semantics and Verification of AADL Modes in Timed Abstract State Machine (regular paper)
In : International Conference on Progress in Informatics and Computing, Shanghai, China, 10/12/10-12/12/10, Vol. 2, IEEExplore digital library, pp. 1098-1103, December 2010.
Marie de Roquemaurel, Thomas Polacsek, Jean-François Rolland, Jean-Paul Bodeveix, Mamoun Filali
Assistance à la conception de modèles à l’aide de contraintes (regular paper)
In : Approches Formelles dans l’Assistance au Développement de Logiciels (AFADL 2010), Poitiers, 09/06/10-11/06/10, Yamine Ait-Ameur (Eds.), LISI-ENSMA, pp. 181-196, June 2010.
Loïc Besnard, Thierry Gautier, Julien Ouy, Jean-Pierre Talpin, Jean-Paul Bodeveix, Alexandre Cortier, Marc Pantel, Martin Strecker, Gérald Garcia, Ana-Helena Rugina, Jérémy Buisson, Fabien Dagnat
Polychronous Interpretation of Synoptic, a Domain Specific Modeling Language for Embedded Flight-Software (regular paper)
In : Workshop on Formal Methods for Aerospace (FMA 2009), Eindhoven, 03/11/09, Vol. 20, Manuela Bujorianu, Michael Fisher (Eds.), Electronic Proceedings in Theoretical Computer Science (EPTCS), pp. 80-87, March 2010.
Bernard Berthomieu, Jean-Paul Bodeveix, Silvano Dal Zilio, Pierre Dissaux, Mamoun Filali, Pierre Gaufillet, Sebastien Heim, François Vernadat
Formal Verification of AADL models with Fiacre and Tina (regular paper)
In : European Congress on Embedded Real-Time Software (ERTS 2010), Toulouse, 19/05/10-21/05/10, SIA/3AF/SEE, (electronic medium), 2010.
URL : http://web1.see.asso.fr/erts2010/Site/0ANDGY78/Fichier/PAPIERS%20ERTS%202010%202/ERTS2010_0107_final.pdf
BibTeXTiago Correa, Leandro Becker, Jean-Paul Bodeveix, J.-M. Farines, Mamoun Filali, François Vernadat
Verification Based Development Process for Embedded Systems (regular paper)
In : European Congress on Embedded Real-Time Software (ERTS 2010), Toulouse, 19/05/10-21/05/10, Société des Ingénieurs de l’Automobile, (electronic medium), May 2010.
URL : http://web1.see.asso.fr/erts2010/Site/0ANDGY78/Fichier/PAPIERS%20ERTS%202010/ERTS2010_0029_final.pdf
BibTeXAlexandre Cortier, Jean-Paul Bodeveix, Marc Pantel, Martin Strecker, Gérald Garcia, Eric Morand, Ana-Helena Rugina, Jean-Pierre Talpin
Synoptic : a Domain Specific Modeling Language for Embed- ded Real-Time Flight Software Design (regular paper)
In : European Conference on Embedded Real Time Software and Systems (ERTS 2010), Toulouse, 19/05/10-21/05/10, SIA/3AF/SEE, (electronic medium), May 2010.
Lei Pi, Jean-Paul Bodeveix, Mamoun Filali, Hu Kai, Ma Dianfu
A comparative study of FIACRE and TASM to define AADL real time concepts
In : UML&AADL’2009 – 14th IEEE International Conference on Engineering of Complex Computer Systems, Postdam, 02/06/09-04/06/09, IEEE : Institute of Electrical and Electronics Engineers, pp. 347-352, June 2009.
URL : http://www2.computer.org/portal/web/csdl/abs/proceedings/iceccs/2009/3702/00/piceccs200900toc.htm
BibTeXRicardo Bedin Franca, Leandro Buss Becker, Jean-Paul Bodeveix, J.-M. Farines, Mamoun Filali
Towards Safe Design of Synchronous Bus Protocols in Event-B (regular paper)
In : Brazilian Symposium on Formal Methods, Gramado Brésil, 19/08/09-21/08/09, Brazilian Computer Society, pp. 171-186, August 2009.
Bernard Berthomieu, Jean-Paul Bodeveix, Christelle Chaudet, Silvano Dal Zilio, Mamoun Filali, François Vernadat
Formal Verification of AADL Specifications in the Topcased Environment
In : International Conference on Reliable Software Technologies – Ada-Europe, Brest, France, 08/06/09-12/06/09, Springer-Verlag, lncs 5570, pp. 207-221, 2009.
Lei Pi, Jean-Paul Bodeveix, Mamoun Filali
Modeling AADL Data Communication with BIP
In : International Conference on Reliable Software Technologies – Ada-Europe, Telecom Bretagne, Brest, France, 08/06/09-12/06/09, Springer-Verlag, lncs 5570, pp. 192-206, 2009.
Lei Pi, Zhibin Yang, Jean-Paul Bodeveix, Mamoun Filali, Kai Hu
A comparative study of two Real-Time formalisms: FIACRE and TASM (regular paper)
In : IEEE Real-Time Systems Symposium (Work-In-Progress track) (RTSS 2008), Barcelone, 30/11/08-03/12/08, IEEE : Institute of Electrical and Electronics Engineers, (electronic medium), December 2008.
Jean-François Rolland, Jean-Paul Bodeveix, Mamoun Filali, David Chemouil, Thomas Dave
AADL modes for space software
In : Data Systems In Aerospace (DASIA 2008), Palma de Majorca-Spain, 27/05/08-30/05/08, European Space Agency (ESA Publications), (electronic medium), May 2008.
Jean-François Rolland, Jean-Paul Bodeveix, Mamoun Filali, David Chemouil, Thomas Dave
Modes in asynchronous systems
In : IEEE International Conference on Engineering Complex Computer Systems (ICECCS 2008), Belfast Ireland, 31/03/08-04/04/08, IEEE : Institute of Electrical and Electronics Engineers, (electronic medium), April 2008.
Frédéric Minot, Jean-Paul Bodeveix, Mamoun Filali, David Doose, Charles Castel, Cédric Pralet, P. Bieber
Constraint-based design of Avionics platform- preliminary design exploration
In : European Congress on Embedded Real-Time Software (ERTS 2008), Toulouse, 31/01/08-01/02/08, Société de l’Electricité, de l’Electronique et des Technologies de l’Information et de la Communication (SEE), (electronic medium), January 2008.
Patrick Farail, Pierre Gaufillet, Florent Peres, Jean-Paul Bodeveix, Mamoun Filali, Bernard Berthomieu, Saad Rodrigo, François Vernadat, Hubert Garavel, Frédéric Lang
FIACRE: an intermediate language for model verification in the TOPCASED environment
In : European Congress on Embedded Real-Time Software (ERTS 2008), Toulouse, 29/01/08-01/02/08, Société de l’Electricité, de l’Electronique et des Technologies de l’Information et de la Communication (SEE), (electronic medium), January 2008.
Jean-François Rolland, Jean-Paul Bodeveix, David Chemouil, Mamoun Filali, Dave Thomas
Towards a formal semantics for AADL execution model
In : European Congress on Embedded Real-Time Software (ERTS 2008), Toulouse, 29/01/08-01/02/08, SIA/3AF/SEE, (electronic medium), January 2008.
Ricardo Bedin Franca, Daniel Gobbi, J.-M. Farines, Jean-Paul Bodeveix, Leandro Becker
Design of Real-Time Automation Systems Using Architecture Description Languages
In : Simpósio Brasileiro de Automação Inteligente (SBAI 2007), Florianópolis – Brasil, 08/08/07-11/08/07, Sociedade Brasileira de Automática (SBA), (electronic medium), August 2007.
Ricardo Bedin Franca, Jean-François Rolland, Jean-Paul Bodeveix, Mamoun Filali
Assessment of AADL’s behavioral annex
In : FAC Formalisation des Activités Concurrentes, Toulouse, 15/03/07-16/03/07.
Ricardo Bedin Franca, Jean-Paul Bodeveix, Mamoun Filali
AADL Modeling of a Generic Bus
In : FAC, Toulouse, 15/03/07-16/03/07.
Julien Brunel, Frédéric Cuppens, Nora Cuppensboulahia, Thierry Sans, Jean-Paul Bodeveix
Security Policy Compliance with Violation Management
In : ACM Workshop on Formal Methods in Security Engineering: From Specifications to Code, Washingthon USA, 12/11/07-13/11/07, ACM : Association for Computing Machinery, pp. 31-40, November 2007.
Jean-Paul Bodeveix, Raphael Cavallero, David Chemouil, Mamoun Filali, Jean-François Rolland
A mapping from AADL to Java-RTSJ
In : International Workshop on Java Technologies for Real-time and Embedded Systems (JTRES 2007), Vienna, Austria, 26/09/07-28/09/07, ACM : Association for Computing Machinery, ACM International Conference Proceeding Series, pp. 165-174, September 2007.
Ricardo Bedin Franca, Jean-Paul Bodeveix, Mamoun Filali, David Chemouil, Dave Thomas
The AADL behaviour annex — experiments and roadmap
In : IEEE International Conference on Engineering Complex Computer Systems (ICECCS 2007), Auckland, New Zealand, 11/07/07-14/07/07, IEEE Computer Society, pp. 377-382, 2007.
Ricardo Bedin Franca, J.-M. Farines, Jean-Paul Bodeveix, Leandro Becker, Mamoun Filali
Modelling a bus protocol an incremental approach
In : Workshop on Real-Time Systems (WTR 2007), Belem (Brésil)l, 28/05/07-28/05/07, Universidade Federal de Santa Catarina, (electronic medium), May 2007.
Jean-Paul Bodeveix, David Chemouil, Mamoun Filali, Nicolas Lalevee, Martin Strecker
Towards the verification of model transformations
In : European Congress on Embedded Real-Time Software (ERTS 2006), Toulouse, 25/01/06-27/01/06, Société des Ingénieurs de l’Automobile, (electronic medium), 2006.
URL : http://www.sia.fr/evenement_detail_erts2006_embedded_real_time_actes_365.htm
BibTeXJean-Paul Bodeveix, Pierre Dissaux, Patrick Farail, Mamoun Filali, Pierre Gaufillet, François Vernadat
Behavioural descriptions in architecture description languages: Application to AADL
In : European Congress on Embedded Real-Time Software (ERTS 2006), Toulouse, 25/01/06-27/01/06, Société des Ingénieurs de l’Automobile, (electronic medium), 2006.
URL : http://www.sia.fr/evenement_detail_erts2006_embedded_real_time_actes_365.htm
BibTeXJean-Paul Bodeveix, Mamoun Filali, Julia Lawall, Gilles Muller
Automatic Verification of Bossa Scheduler Properties
In : nternational Workshop on Automated Verification of Critical Systems (AVOCS 2006), LORIA Nancy, 18/09/06-19/09/06, Archives ouvertes HAL, (on line), September 2006.
URL : http://hal.inria.fr/
BibTeXJulien Brunel, Jean-Paul Bodeveix, Mamoun Filali
A state/event temporal deontic logic
In : Journées FAC’06, Toulouse, 23/03/06-24/03/06.
Jean-Paul Bodeveix, Pierre Dissaux, Mamoun Filali, Pierre Gaufillet, François Vernadat
AADL behavioural annex
In : Data Systems In Aerospace (DASIA 2006), Berlin-Germany, 22/05/06-25/05/06, European Space Agency (ESA Publications), (electronic medium), 2006.
Jean-Paul Bodeveix, Mamoun Filali, Miloud Rached, David Chemouil, Pierre Gaufillet
Experimenting an AADL Behavioural Annex and a Verification Method
In : Data Systems In Aerospace (DASIA 2006), Berlin-Germany, 22/05/06-25/05/06, European Space Agency (ESA Publications), (electronic medium), 2006.
Julien Brunel, Jean-Paul Bodeveix, Mamoun Filali
A state/event temporal deontic logic
In : International Workshop on Deontic Logic in Computer Science (DEON 2006), Utrecht, The Netherlands, 12/07/06-14/07/06, Vol. , Lou Goble, John-Jules Ch. Meyer (Eds.), Springer, LNAI 4048, pp. 85-100, July 2006.
Jean-Paul Bodeveix, Mamoun Filali, Julia Lawall, Gilles Muller
Vérification automatique de propriétés d’ordonnanceurs Bossa
In : Approches Formelles dans l’Assistance au Développement de Logiciels (AFADL 2006), ENST Paris, 15/03/06-17/03/06, ENST, pp. 95-109, March 2006.
Odile Nasr, Jean-Paul Bodeveix, Mamoun Filali, Miloud Rached
Développement validé d’odonnanceurs en B
In : Approches Formelles dans l’Assistance au Développement de Logiciels (AFADL 2006), ENST Paris, 15/03/06-17/03/06, ENST, pp. 79-93, March 2006.
Odile Nasr, Jean-Paul Bodeveix, Mamoun Filali, Miloud Rached
Verification of a Scheduler in B Through a Timed Automata Specification
In : Annual ACM Symposium on Applied Computing (SAC 2006), Dijon, 23/04/06-27/04/06, ACM : Association for Computing Machinery, pp. 1800-1801, April 2006.
Miloud Rached, Jean-Paul Bodeveix, Mamoun Filali, Odile Nasr
Real Time Aspects: Specification and Composition in B
In : 7th International Workshop on Aspect-Oriented Modeling, Montego Bay, Jamaica, 02/10/05-02/10/05, ?, October 2005.
URL : http://dawis.informatik.uni-essen.de/events/AOM_MODELS2005/papers.shtml
BibTeXJean-Paul Bodeveix, Mamoun Filali, Julia Lawall, Gilles Muller
Applying the B formal method to the Bossa domain-specific language
In : The 17th Nordic Workshop on Programming Theory, Copenhagen, Denmark, 19/10/05-21/10/05, DIKU Copenhagen, Denmark, October 2005.
Miloud Rached, Jean-Paul Bodeveix, Mamoun Filali, Odile Nasr
A Timed B Method for Modelling Real Time Reactive Systems
In : SEEFM05. 2nd South-East European Workshop on Formal Methods, Ohrid (Macédoine), 18/11/05-20/11/05, South-East European Research Center (SEERC), pp. 181-195, November 2005.
Jean-Paul Bodeveix, Ousmane Koné, Rachid Bouaziz
Test method for embedded real-time systems
In : ERCIM European Workshop on Dependable Software Intensive Embedded Systems, Porto, 31/08/05-02/09/05, ERCIM, pp. 1-10, August 2005.
Richard Banach, Jean-Paul Bodeveix, Mamoun Filali, Michael Poppleton
Dynamic aspects of retrenchments through temporal logic
In : SEEFM05 2nd South-East European Workshop on Formal Methods, Ohrid (Macédoine), 18/11/05-19/11/05, South-East European Research Center (SEERC), pp. 104-118, November 2005.
Jean-Paul Bodeveix, Mamoun Filali, Julia Lawall, Gilles Muller
Formal methods meet domain specific languages
In : Fifth International Conference on Integrated Formal Methods (IFM), Eindhoven Netherlands, 29/11/05-02/12/05, LNCS (springer verlag) Vol. 3771, pp. 187-206, November 2005.
Jean-Paul Bodeveix, David Chemouil, Mamoun Filali, Martin Strecker
Towards formalizing AADL in proof assistants
In : Formal Foundations of Embedded software and component-based softare architectures (ETAPS), Edinburgh, 02/04/05-10/04/05, Juliana Kuster-Filipe, Iman Poernomo , Ralf Reussner, Sandeep Shukla (Eds.), LFCS (University of Edinburgh), pp. 137-153, April 2005.
Jean-Paul Bodeveix, Mamoun Filali, Martin Strecker
Towards formalising AADL in Proof Assistants
In : Journées FAC’05, Toulouse LAAS, 09/03/05-10/04/05.
Odile Nasr, Miloud Rached, Jean-Paul Bodeveix, Mamoun Filali
Specification of real-time schedulers
In : 16th Euromicro Conference on Real-Time Systems (ECRTS’04) (Work In Progress Session), Catania, Italy, 30/06/04-02/07/04, -, June 2004.
Nouhad Amaneddine, Jean-Paul Bahsoun, Jean-Paul Bodeveix
Vers une transformation avancée de données structurées
In : MAJESTIC, Calais, France, 13/10/04-15/10/04, Maison de la Recherche Blaise Pascal, October 2004.
Nouhad Amaneddine, Jean-Paul Bahsoun, Jean-Paul Bodeveix
TransM: A Structured Document Transformation Model
In : 3rd International Conference on Information Systems Technology and its Applications (ISTA), Salt Lake City, Utah, USA, 15/07/04-17/07/04, Lecture Notes in Informatics, pp. 53-66, July 2004.
Jean-Paul Bodeveix, Mamoun Filali, Odile Nasr
Spécification d’ordonnanceurs temps réel
In : FAC, Toulouse, 09/03/04-10/03/04.
Jean-Paul Bodeveix, Mamoun Filali, Miloud Rached
Méthodes de spécification de systèmes temps réel en B
In : FAC, Toulouse, 09/03/04-10/03/04.
Jean-Paul Bodeveix, Mamoun Filali
About disjunctive invariants in UPPAAL
In : NWPT, Turku Finlande, 29/10/03-31/10/03.
Pierre Bazex, Jean-Paul Bodeveix, Christophe Le Camus, Thierry Millan, Christian Percebois
Vérification de modèles UML fondée sur OCL
In : INFORSID, Nancy, 03/06/03-06/06/03, Congrès INFormatique des ORganisations et Systèmes d’Information et de Décision (INFORSID), pp. 185-200, June 2003.
Bernard Berthomieu, P.-O. Ribet, François Vernadat, J.-L. Bernartt, J.-M. Farines, Jean-Paul Bodeveix, Mamoun Filali, Gérard Padiou, Pierre Michel, Patrick Farail, Pierre Gaufillet, Pierre Dissaux, Jean-Luc Lambert
Towards the verification of real-time systems in avionics: TheCotre approach
In : Eigth International workshop for industrial critical systems, ROROS, 05/06/03-07/06/03, Thomas Arts, Wan Fokkink, pp. 201-216, June 2003.
URL : http://www.elsevier.nl/locate/entcs/volume80.html
BibTeXJ.-M. Farines, Bernard Berthomieu, Jean-Paul Bodeveix, Pierre Dissaux, Patrick Farail, Mamoun Filali, Pierre Gaufillet, Hicham Hafidi, Jean-Luc Lambert, Pierre Michel, François Vernadat
The Cotre project: rigorous development for real time systems in Avionics
In : WRTP’03 27th IFAC/IFIP/IEEE Workshop on real-time programming, Logow(Pologne), 14/05/03-17/05/03, IEEE, pp. 51-56, May 2003.
Jean-Paul Bodeveix, Mamoun Filali
Machines virtuelles pour le B événementiel
In : AFADL, Rennes, 15/01/03-17/01/03, Jean-Marc Jézéquel, INRIA, pp. 227-241, January 2003.
URL : http://www.irisa.fr/manifestations/2003/AFADL03
BibTeXJean-Paul Bodeveix, Mamoun Filali
Machines virtuelles pour le B événementiel
In : Journées GDR B, Paris, 13/06/02-14/06/02.
URL : http://www-lsr.imag.fr/B/Documents/CNAM-2002-06-13/prog-CNAM-2002.html
BibTeXJean-Paul Bodeveix, Mamoun Filali, Semra Sarpdag
Etude des files de priorité
In : journée GDR B, Nantes, 29/11/02-29/11/02.
URL : http://www-lsr.imag.fr/B/Documents/Nantes-2002-11-29/prog.html
BibTeXJean-Paul Bodeveix, Mamoun Filali
Un outil pour la description de types inductifs en B
In : journée du GDR B, Nantes, 29/11/02-29/11/02.
URL : http://www-lsr.imag.fr/B/Documents/Nantes-2002-11-29/prog.html
BibTeXJean-Paul Bodeveix, Thierry Millan, Christian Percebois, Christophe Le Camus, Pierre Bazex, Louis Féraud, Ralph Sobek
Extending OCL for verifying UML models consistency
In : Workshop on Consistency Problems in UM- based Software Development in conjonction with the fifth International Conference on the Unified Modelling Language “UML” 2002 “Modelling Languages, Concepts and Tools”, Dresden, Allemagne, 01/10/02, Ludwik Kuzniarz – Gianna Reggio – Jean-Louis Sourrouille – Zbigniew Huzar, pp. 75-91, October 2002.
Jean-Paul Bodeveix, Mamoun Filali
Type Synthesis in B and the Translation of B to PVS
In : ZB’2002, Grenoble, 23/01/02-25/01/02, springer verlag, pp. 350-369, January 2002.
Jean-Paul Bodeveix, Mamoun Filali, Cesar Munoz
Formalisation de la méthode B en Coq et PVS
In : AFADL, Grenoble, 26/01/00-28/01/00, LSR/IMAG, pp. 96-110, January 2000.
Pierre Bazex, Jean-Paul Bodeveix, Louis Féraud, Thierry Millan
Modélisation et transformations de données
In : Journées sur les technologies applicables à la valorisation de données, Toulouse, .
Pierre Bazex, Jean-Paul Bodeveix, Louis Féraud, Thierry Millan, Christian Percebois
Data Design and Transformation
In : World Multiconference on Systemics, Cybernetics and Informatics 2000, Orlando (USA), 23/07/00-26/07/00, IIIS, 14269 Lord Barclay Dr., Orlandom FL 32837, USA, pp. 587-592, July 2000.
Jean-Paul Bodeveix, Mamoun Filali, Daniel Le Berre
Expression de méthodes de validation. Transformation en logique propositionnelle ou monadique
In : Journées de VERIFICATION FORMELLE, ORLEANS, 08/06/00-09/06/00.
URL : http://www.univ-orleans.fr/SCIENCES/LIFO/Manifestations/Jo-VERIF/
BibTeXJean-Paul Bodeveix, Mamoun Filali
Expérimentation de méthodes d’accélération pour la validation de systèmes paramétrés
In : FAC’2000, Toulouse, 18/05/00, IRIT, pp. 19-29, May 2000.
Jean-Paul Bodeveix, Mamoun Filali
FMona: a tool for expressing validation techniques over infinite state systems
In : Tools and algorithms for the construction and analysis of systems (TACAS), Berlin, 27/03/00-31/03/00, Springer, pp. 204-219, March 2000.
Salam Majoul, Christian Percebois, Jean-Paul Bodeveix
A Concurrent Object-Based Model and its Use for Coordinating Java Components
In : TOOLS – Technology of Object-Oriented Languages and Systems, Santa Barbara, 01/08/99-05/08/99, IEEE, pp. 15-25, August 1999.
Jean-Paul Bodeveix, Mamoun Filali
Un outil générique pour l’expression de méthodes de validation
In : Journées Modélisation et Vérification, Besançon, 09/12/99-11/12/99.
Jean-Paul Bodeveix, Mamoun Filali, Cesar Munoz
Mécanisation de la méthode B en Coq et PVS
In : Journées BUG-SEE, LILLE, 29/11/99-30/11/99.
Jean-Paul Bodeveix, Mamoun Filali, Cesar Munoz
A Formalization of the B method in Coq and PVS
In : FM’99 — B Users Group Meeting — Applying B in an industrial context : Tools, Lessons and Techniques, Toulouse, Springer-Verlag, pp. 32-48, September 1999.
Jean-Paul Bodeveix, Mamoun Filali
A generic tool for expressing the development of validations
In : 11th Nordic Workshop on Programming Theory NWPT’99, Uppsala, 06/10/99-08/10/99, Bjorn Victor and Wang Yi, Uppsala University, pp. 37-37, October 1999.
Jean-Paul Bodeveix, Mamoun Filali
Preuve automatique par abstraction de problèmes à espace d’états infini ou paramétrés
In : Formalisation des activités concurrentes, LAAS Toulouse, 25/02/99-26/02/99, LAAS, pp. 19-30, February 1999.
Jean-Paul Bodeveix, Mamoun Filali
On the automatic validation of parameterized Unity programs
In : Workshop on formal methods for parallel programming: theory and applications, Orlando , 03/04/98-03/04/98, lncs vol. 1388, Berlin, Germany, pp. 820-832, April 1998.
Jean-Paul Bodeveix, Mamoun Filali
Expériences de preuves assistées et automatiques de problèmes paramétrés
In : Journées Modélisation et Vérification, CIRM, Marseille, 16/12/98-18/12/98.
Salam Majoul, Christian Percebois, Jean-Paul Bodeveix
Reasoning about Negative Conditions in a Concurrent Rewriting System
In : 2nd France-Japan Workshop on Object-Based Parallel and Distributed Computation, Toulouse, .
Jean-Paul Bodeveix, Mamoun Filali
Preuve automatique de propriétés de sureté
In : GDR de Programmation – Journées du pôle Preuves et Spécifications Algébriques, –, .
Jean-Paul Bodeveix, Mamoun Filali
Validation de développements
In : AFADL Approches formelles dans l’assistance au développement de logiciels, CERT Toulouse, GDR de Programmation: Pôle preuves et spécifications algébriques, pp. 165-176, May 1997.
Jean-Paul Bodeveix, Dominique Carrière, Mamoun Filali
A refinement-based validation of a cache coherence protocol
In : 10th International Conference on Parallel and Distributed Computing Systems, New Orleans, Louisiana USA, ISCA, pp. 332-337, October 1997.
Jean-Paul Bodeveix, Christian Percebois, Salam Majoul
An object oriented coordination model based on multiset rewriting
In : Procs. of ninth International Conference on Parallel and Distributed Computing Systems, Dijon, 25/09/96-27/09/96, isca, pp. 1-12, September 1996.
Jean-Paul Bodeveix, Mamoun Filali
Formalisation et validation de protocoles de cohérence mémoire atomique
In : École ISYPAR, IRIT, .
Jean-Paul Bodeveix, Mamoun Filali
Spécification et raffinement de modèles de cohérence mémoire
In : FAC96: Formalisation des Applications Concurrentes, Toulouse, 07/02/96-08/02/96, -, February 1996.
Jean-Paul Bodeveix, Dominique Carrière, Mamoun Filali
Etude du protocole de cohérence de la machine M3S
In : Rencontres du parallélisme RenPar’8, –, -, pp. 173-176, May 1996.
Jean-Paul Bodeveix, Mamoun Filali
Spécification et raffinement de modèles de cohérence mémoire
In : Modélisation des systèmes réactifs, –, AFCET, March 1996.
Jean-Paul Bodeveix, Mamoun Filali
Towards the automatic verification of memory protocols
In : International Workshop on Formal methods for parallel programming, _, IEEE, April 1996.
Jean-Paul Bodeveix, Christian Percebois, Salam Majoul
Multiset Rewriting for Concurrent Object-Oriented Programming
In : ECOOP’96 Workshop on Proof Theory of Concurrent Object-Oriented Programming, Linz, Austria, -, July 1996.
Jean-Paul Bodeveix, Mamoun Filali
On the Refinement of Symmetric Memory Protocols
In : Higher Order Logic Theorem Proving and its Applications, –, Springer-Verlag, LNCS 971, pp. 58-74, September 1995.
Jean-Paul Bodeveix, Mamoun Filali, Pierre Roché
Sémantique des modèles de consistance mémoire
In : Journée du pôle preuves et spécifications algébriques du GDR programmation, –, .
Jean-Paul Bodeveix, Mamoun Filali, Pierre Roché
Towards a HOL theory of memory
In : Higher Order Logic Theorem Proving and its Applications, –, Springer-Verlag, LNCS 859, pp. 49-64, September 1994.
Juan-Carlos Cruellas, Jean-Paul Bodeveix, Thierry Millan, Agusti Canals
The NEPTUNE Technology to verify and to Document Software cOMPONENTS
In : Business Component-Based Software Engineering. Franck Barbier (Eds.) , Kluwer Academic Publishers, Post Office Box 322 – 330 AH Dordrecht – THE NETHERLANDS, pp. 101-118, 2003.
Méthodes formelles et sûreté de développement
HDR, Université Paul Sabatier, October 2001.
Abdeldjalil Boudjadar, Jean-Paul Bodeveix, Mamoun Filali
Revising and Extending the Uppaal Communication Mechanism, Springer-Verlag, Vol. 7306, Lecture Notes in Computer Science, June 2012.
J.-M. Farines, Bernard Berthomieu, Jean-Paul Bodeveix, Pierre Dissaux, Patrick Farail, Mamoun Filali, Pierre Gaufillet, Hicham Hafidi, Jean-Luc Lambert, Pierre Michel, François Vernadat
The Cotre Project: Rigorous Software Development for Real Time Systems in Avionics, COLNARIC, ADAMSKI & WEGRZYN, November 2003.
Jean-Paul Bodeveix, Thierry Millan, Christian Percebois, Pierre Bazex, Louis Féraud
NEPTUNE : Method, Checking and documentation generation for UML application
, NEPTUNE Consortium, 2003.
Jean-Paul Bodeveix, Mamoun Filali, Amal Sayah
Programmation en C++, InterEditions, 1994.
Bernard Berthomieu, Jean-Paul Bodeveix, Silvano Dal Zilio, Mamoun Filali, François Vernadat
Vérification formelle de spécifications AADL via FIACRE
Diffusion pédagogique. August 2011.
Jean-Paul Bodeveix, Mamoun Filali, Thomas Polacsek
Projet PAM: AIde à la conception d’une palte-forme avionique
Présentation orale. March 2009.